/*
 * $Id: Checker.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jiri Adamek <adamek@nenya.ms.mff.cuni.cz>
 *
 */

package org.objectweb.fractal.bpc.staticchecker;

import java.util.Map;
import java.util.HashMap;
import java.util.Set;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Arrays;
import java.util.Comparator;


import org.objectweb.fractal.bpc.staticchecker.preprocessor.Debug;
import org.objectweb.fractal.bpc.staticchecker.preprocessor.InterfaceMapBuilder;
import org.objectweb.fractal.bpc.staticchecker.preprocessor.Node;
import org.objectweb.fractal.bpc.staticchecker.preprocessor.ParseErrorException;
import org.objectweb.fractal.bpc.staticchecker.preprocessor.Parser;
import org.objectweb.fractal.bpc.staticchecker.preprocessor.SynchroSetBuilder;
import org.objectweb.fractal.bpc.staticchecker.preprocessor.Transformation;
import org.objectweb.fractal.bpc.staticchecker.preprocessor.TransformationErrorException;

/**
 * This is the entry point of the Fractal static BP-checker wrapper. 
 * 
 * To do the checking, call the {@link #check(FrameInstance, FrameInstance[], Binding[])} method of this class. 
 * As parameters, the method takes description of one level of hierarchical component structure of a Fractal application, i.e.:
 * <ul>
 * <li>frame description of a component C</li>
 * <li>frame instance descriptions all C's direct subcomponents</li>
 * <li>
 * descriptions of all interface ties in C's architecture, i.e. bindings among C's direct subcomponents
 * AND subsumptions/delegations between C's interfaces and interfaces of direct C's subcomponents
 * </li>
 * </ul>
 * Every frame instance description consists of:
 * <ul>
 * <li>the name of the frame instance</li>
 * <ul>
 * <li><em>IMPORTANT:</em> For the frame of C itself, <code>null</code> has to be set instead of the name</li>
 * <li><em>IMPORTANT:</em> The names of frame instances have to be unique</li>
 * </ul>
 * <li>descriptions of the interface instances of the frame instance</li>
 * </ul>
 * Every interface instance description consists of:
 * <ul>
 * <li>the name of the frame instance the interface instance is contained in</li>
 * <li>the name of the interface instance</li>
 * <ul><li><em>IMPORTANT:</em> The names of frame interface instances within a frame instance have to be unique</li></ul>
 * <li>the boolean flag telling whether the interface instance is provided (or required)</li>
 * <li>the array of method names</li>
 * </ul> 
 * The {@link #check(FrameInstance, FrameInstance[], Binding[])} method does the following: 
 * <ul>
 * <li>
 * the frame protocols of both C and its direct subcomponents are parsed; parse errors, 
 * unknown names, etc. are identified and reported
 * </li>
 * <li>
 * in several steps the transformations of the protocols are done to address the following features:
 * <ul>
 * <li>collection interfaces</li>
 * <li>multiple bindings</li>
 * </ul>
 * <li>event sets for the protocol composition and events on unbound interfaces are identified</li>
 * <li>
 * standalone behavior protocol checker is launched, 
 * the transformed protocols and identified event sets are used as parameters,
 * the result of the checking is reported
 * </li> 
 */
public class Checker {

	/**
	 * This method checks the behavior of a Fractal component.
	 * In more detail, it does the following: 
	 * <ul>
	 * <li>
	 * the frame protocols of both a component and its direct subcomponents are parsed; parse errors, 
	 * unknown names, etc. are identified and reported
	 * </li>
	 * <li>
	 * in several steps the transformations of the protocols are done to address the following features:
	 * <ul>
	 * <li>collection interfaces</li>
	 * <li>multiple bindings</li>
	 * </ul>
	 * <li>event sets for the protocol composition and events on unbound interfaces are identified</li>
	 * <li>
	 * standalone behavior protocol checker is launched, 
	 * the transformed protocols and identified event sets are used as parameters,
	 * the result of the checking is reported
	 * </li> 
	 * 
	 * @param superComponent description of the frame instance of a component C 
	 * @param subcomponents frame instance descriptions of direct subcomponent of C
	 * @param bindings bindings in the archotecture of C (including delegations and subsumptions)
	 * @return the checking result
	 */
	public static CheckingResult check(FrameInstance superComponent,
			FrameInstance[] subcomponents, Binding[] bindings) {
		
		/* 
		 * Reorder the subcomponents according the values of the "order"
		 * item.
		 */
		
		Arrays.sort(subcomponents, new Comparator() {
			public int compare(Object o1, Object o2) {
				FrameInstance f1 = (FrameInstance)o1;
				FrameInstance f2 = (FrameInstance)o2;
				return f1.order < f2.order ? -1 : (f1.order > f2.order ? 1 : 0);
			}
		});
		
		/* Initialize the parser */
		
		Parser parser = new Parser();

		/* Parse protocols of subcomponents */

		Node subcomponentParseTrees[] = new Node[subcomponents.length];
		
		for (int i = 0; i < subcomponents.length; i++)
			try {
				subcomponentParseTrees[i] = parser.parse(subcomponents[i]);
			} catch (ParseErrorException e) {
				return new CheckingResult(CheckingResult.ERR_NOT_CHECKED, e
						.getMessage());
			}

		/* Parse the protocol of the super-component */

		Node superComponentParseTree;
			
		try {
			superComponentParseTree = parser.parse(superComponent);
		} catch (ParseErrorException e) {
			return new CheckingResult(CheckingResult.ERR_NOT_CHECKED, e
					.getMessage());
		}

		/* Construct the interface maps and identify unbound interfaces */
		
		Map interfaceMap = new HashMap();
		Map reverseInterfaceMap = new HashMap();
		Set unboundProvidedInterfaces = new HashSet();
		Set unboundRequiredInterfaces = new HashSet();
		
		InterfaceMapBuilder.build(interfaceMap, reverseInterfaceMap,
				unboundProvidedInterfaces, unboundRequiredInterfaces,
				superComponent, subcomponents, bindings);    
	    
	    /* Do the transformation */
	    
	    Transformation transformation = new Transformation(interfaceMap, reverseInterfaceMap);
		
	    /* Transform the protocol of the super-component */
	    
	    try {
	    	superComponentParseTree = transformation.transform(superComponentParseTree, superComponent);
	    } catch(TransformationErrorException e) {
	    	return new CheckingResult(CheckingResult.ERR_NOT_CHECKED, e
					.getMessage());
	    }
	    
	    /* Transform protocols of subcomponents */

		for (int i = 0; i < subcomponents.length; i++)
			try {
				subcomponentParseTrees[i] = transformation.transform(
						subcomponentParseTrees[i], subcomponents[i]);
			} catch (TransformationErrorException e) {
				return new CheckingResult(CheckingResult.ERR_NOT_CHECKED, e
						.getMessage());
			}

		/* Compute the synchro-event sets and the unbound-event set */
		
		String unboundEvents = SynchroSetBuilder.getUnboundEvents(
				unboundProvidedInterfaces, unboundRequiredInterfaces);
		
		String[] synchroSets = SynchroSetBuilder.getSynchroSets(superComponent,
				subcomponents, bindings, interfaceMap, reverseInterfaceMap);
			
		/* Debug: print the content of the interface maps */
					
		Debug.print(debugLevel, "Interface map:\n");
		Debug.print(debugLevel, "--------------\n");
		debugPrintInterfaceMap(interfaceMap);
		Debug.print(debugLevel, "\n");
		
		Debug.print(debugLevel, "Reverse interface map:\n");
		Debug.print(debugLevel, "----------------------\n");
		debugPrintInterfaceMap(reverseInterfaceMap);
		Debug.print(debugLevel, "\n");
		
		/* Debug: print the content of the sets of unbound interfaces */
		
		Debug.print(debugLevel, "Unbound provided interfaces:\n");
		Debug.print(debugLevel, "----------------------------\n");
		debugPrintInterfaceSet(unboundProvidedInterfaces);
		Debug.print(debugLevel, "\n");
		
		Debug.print(debugLevel, "Unbound required interfaces:\n");
		Debug.print(debugLevel, "----------------------------\n");
		debugPrintInterfaceSet(unboundRequiredInterfaces);
		Debug.print(debugLevel, "\n");
		
		/* Debug: print the results of protocol transformations */

		Debug.print(debugLevel, "The protocols (before ==> after):\n");
		Debug.print(debugLevel, "---------------------------------\n\n");
		
		Debug.print(debugLevel, "The supercomponent:\n");
		Debug.print(debugLevel, superComponent.protocol + "\n==>\n");
		Debug.print(debugLevel, superComponentParseTree.toString() + "\n\n");
		
		for (int i = 0; i < subcomponents.length; i++) {
			Debug.print(debugLevel, "The '" + subcomponents[i].frameName + "' subcomponent: \n");
			Debug.print(debugLevel, subcomponents[i].protocol + "\n==>\n");
			Debug.print(debugLevel, subcomponentParseTrees[i].toString() + "\n\n");
		}
		
		Debug.print(debugLevel, "Events on unbound interfaces:\n");
		Debug.print(debugLevel, "-----------------------------\n");
		Debug.print(debugLevel, unboundEvents + "\n\n");
		
		Debug.print(debugLevel, "Synchro-sets:\n");
		Debug.print(debugLevel, "-------------\n");
		for (int i = 0; i < synchroSets.length; i++)
			Debug.print(debugLevel, i + ": " + synchroSets[i] + "\n");
		Debug.print(debugLevel, "\n");
		
		/* Run the checker core */
		String[] subcomponentProtocols = new String[subcomponents.length];
		for (int i = 0; i < subcomponents.length; i++)
			subcomponentProtocols[i] = subcomponentParseTrees[i].toString();

		org.objectweb.fractal.bpc.checker.FractalStaticChecker checkerCore = 
			new org.objectweb.fractal.bpc.checker.FractalStaticChecker();
		
		org.objectweb.fractal.bpc.checker.CheckingResult coreResult = checkerCore
				.check(superComponentParseTree.toString(), synchroSets,
						subcomponentProtocols, unboundEvents);
		
		return transformResult(coreResult); 
		
	}

	private static CheckingResult transformResult(org.objectweb.fractal.bpc.checker.CheckingResult coreResult) {
		
		switch(coreResult.type) {
		
		case org.objectweb.fractal.bpc.checker.CheckingResult.ERR_OK:
			return new CheckingResult(CheckingResult.ERR_OK, coreResult.description);
			
		case org.objectweb.fractal.bpc.checker.CheckingResult.ERR_BADACTIVITY:
			return new CheckingResult(CheckingResult.ERR_BADACTIVITY, coreResult.description);
		
		case org.objectweb.fractal.bpc.checker.CheckingResult.ERR_NOACTIVITY:
			return new CheckingResult(CheckingResult.ERR_NOACTIVITY, coreResult.description);
		
		case org.objectweb.fractal.bpc.checker.CheckingResult.ERR_INFINITEACTIVITY:
			return new CheckingResult(CheckingResult.ERR_DIVERGENCE, coreResult.description);
		
		case org.objectweb.fractal.bpc.checker.CheckingResult.ERR_SYNTAXERROR:
			return new CheckingResult(CheckingResult.ERR_NOT_CHECKED, "INTERNAL SYNTAX ERROR: " + coreResult.description);
		
		case org.objectweb.fractal.bpc.checker.CheckingResult.ERR_OTHERERROR:
			return new CheckingResult(CheckingResult.ERR_NOT_CHECKED, "OTHER INTERNAL ERROR: " + coreResult.description);
		
		default:
			return new CheckingResult(CheckingResult.ERR_NOT_CHECKED, "UNKNOWN INTERNAL ERROR: " + coreResult.description);
		}
	}
	
	private static void debugPrintInterfaceSet(Set set) {
		Iterator it = set.iterator();
		while (it.hasNext()) {
			InterfaceInstance inInst = (InterfaceInstance) it.next();
			Debug.print(debugLevel, (inInst.frameName == null ? "" : inInst.frameName) + ":" + inInst.interfaceName + "\n");
		}
	}

	private static void debugPrintInterfaceMap(Map map) {
		Iterator it = map.entrySet().iterator();
		while (it.hasNext()) {
			Map.Entry entry = (Map.Entry) it.next();
			InterfaceInstance inInst = (InterfaceInstance)entry.getKey();
			Debug.print(debugLevel, (inInst.frameName == null ? "" : inInst.frameName) + ":" + inInst.interfaceName + "\n");
			Iterator it2 = ((Set)entry.getValue()).iterator();
			while (it2.hasNext()) {
				InterfaceInstance inInst2 = (InterfaceInstance)it2.next();
				Debug.print(debugLevel, "   " + (inInst2.frameName == null ? "" : inInst2.frameName) + ":" + inInst2.interfaceName + "\n");	
			}	
		}
	}

	private static final int debugLevel = 2;
	
}
